﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace PSZT
{
    public class Model
    {
        public List<Predykat> dostepnePredykaty = new List<Predykat>();
        public List<Formula> baza = new List<Formula>();
        public Formula doUdowodnienia;

        public Model()
        {

        }

        public int dodajPredykat(Predykat predykat)
        {
            dostepnePredykaty.Add(predykat);
            return 0;
        }

        public int usunWszystkieDostepnePredykaty()
        {
            dostepnePredykaty.Clear();
            return 0;
        }

        public bool wnioskujWPrzod()
        {
            int liczbaNowychLiteralow;
            bool jestLiteralUdowadniajacy;
            do
            {
                List<Formula> noweLiteraly = new List<Formula>();
                liczbaNowychLiteralow = 0;

                foreach (Formula formula in baza.Where(x => x.czyLiteral() == false))
                {
                    List<Podstawienie>[] sensownePodstawienia = new List<Podstawienie>[formula.przeslanki.Count];
                    for (int i = 0; i < formula.przeslanki.Count; ++i)
                    {
                        sensownePodstawienia[i] = new List<Podstawienie>();
                    }

                    //Znajdowanie sensownych podstawień
                    //czyli takich, dla których istnieją literały udowadniające daną przesłankę
                    for (int i = 0; i < formula.przeslanki.Count; ++i)
                    {
                        Predykat przeslanka = formula.przeslanki[i];
                        foreach (Formula literal in baza.Where(x => x.czyLiteral()))
                        {
                            if (literal.konkluzja.jestUnifikowalnyZ(przeslanka))
                            {
                                sensownePodstawienia[i].Add(przeslanka.znajdzPodstawienia(literal.konkluzja));
                            }
                        }
                    }

                    //Jeżeli któraś z przesłanek nie ma udowadniającego ją literału to przejdź do następnej formuły
                    bool nastepnaFormula = false;
                    foreach (List<Podstawienie> listaPodstawien in sensownePodstawienia)
                    {
                        if (listaPodstawien.Count == 0)
                        {
                            nastepnaFormula = true;
                            break;
                        }
                    }
                    if (nastepnaFormula)
                        continue;

                    int[] stosPodstawien = new int[formula.przeslanki.Count];

                    stosPodstawien[0] = 0;
                    for (int i = 1; i < formula.przeslanki.Count; ++i)
                    {
                        stosPodstawien[i] = -1;
                    }

                    
                    List<int[]> poprawneUstawieniaStosu = new List<int[]>();
                    do
                    {
                    //1. Sprawdzić czy występuje konflikt w listach na stosie
                    //1a. Jeśli tak:
                    //    - zwiekszyc wartosc pod aktualnym indeksem
                    //             - jezeli nie mozna to zwiekszyc poprzedni itd.
                    //1b. Jesli nie:
                    //    - jezeli uzyto podstawien dla wszystkich przeslanek (nie ma -1 w tablicy)
                    //       to dodaj do listy poprawnych
                    //     - jezeli nie uzyto
                    //       to zwieksz indeks i zwieksz wartosc pod indeksem
                        if (CzyWystepujaKonflikty(stosPodstawien, sensownePodstawienia) == false && stosPodstawien.All(x=> x != -1))
                        {
                            poprawneUstawieniaStosu.Add(stosPodstawien.Clone() as int[]);
                        }
                    } while (nowyStanStosu(ref stosPodstawien, sensownePodstawienia) == true);

                    foreach (int[] ustawieniaStosu in poprawneUstawieniaStosu)
                    {
                        Formula nowyliteral = new Formula();
                        nowyliteral.konkluzja = formula.konkluzja.podstaw(ustawieniaStosu, sensownePodstawienia);
                        if (nowyliteral.konkluzja != null)
                        {
                            if (!baza.Contains(nowyliteral))
                            {
                                noweLiteraly.Add(nowyliteral);
                                liczbaNowychLiteralow++;
                            }
                        }
                    }
                }

                baza.AddRange(noweLiteraly);

                //Sprawdzanie czy już udowodniono
                jestLiteralUdowadniajacy = false;
                foreach (Formula f in baza.Where(x => x.przeslanki.Count == 0)) {
                    if (f.konkluzja.jestUnifikowalnyZ(doUdowodnienia.konkluzja))
                    {
                        jestLiteralUdowadniajacy = true;
                        return true;
                    }
                }
            } while (liczbaNowychLiteralow > 0 && !jestLiteralUdowadniajacy);

            return false;
        }

        private bool nowyStanStosu(ref int[] stosPodstawien, List<Podstawienie>[] sensownePodstawienia, int depth = 0)
        {
            int index = stosPodstawien.Length - depth - 1;

            if (index < 0)
            {
                stosPodstawien[0] = -1;
                return false;
            }

            if (stosPodstawien[index] + 1 < sensownePodstawienia[index].Count)
            {
                stosPodstawien[index]++;
                return true;
            }
            else
            {
                stosPodstawien[index] = -1;
                return nowyStanStosu(ref stosPodstawien, sensownePodstawienia, depth + 1);
            }
        }

        private bool nowyStanStosu2(ref int[] stosPodstawien, List<Podstawienie>[] sensownePodstawienia)
        {
            int indeks = 0;
            if (stosPodstawien[0] == -1)
            {
                return false;
            }

            while (stosPodstawien.Count()-1 > indeks && stosPodstawien[indeks] > -1)
                indeks++;

            if (stosPodstawien[indeks] + 1 < sensownePodstawienia[indeks].Count)
            {
                stosPodstawien[indeks]++;
                return true;
            }
            else
            {
                stosPodstawien[indeks] = -1;
                return nowyStanStosu(ref stosPodstawien, sensownePodstawienia);
            }
        }

        private bool CzyWystepujaKonflikty(int[] stos, List<Podstawienie>[] tablicaPodstawien)
        {
            List<Podstawienie> uzywanePodstawienia = new List<Podstawienie>();
            for (int i = 0; i < stos.Count(); ++i)
            {
                // Dodaje do listy uzywanych podstawien: podstawienie z tablicy sensownych podstawien, gdzie i to numer przeslanki, a stos[i] to numer podstawienia z listy (dla tej przeslanki)
                if (stos[i] > -1)
                    uzywanePodstawienia.Add(tablicaPodstawien[i][stos[i]]);
            }

            Dictionary<string, string> uzywaneZmienne = new Dictionary<string, string>();
            foreach (Podstawienie p in uzywanePodstawienia)
            {
                foreach (KeyValuePair<string, string> pair in p.podstawienia)
                {
                    if (uzywaneZmienne.ContainsKey(pair.Key))
                    {
                        if (uzywaneZmienne[pair.Key] != pair.Value)
                            return true;
                    }
                    else
                    {
                        uzywaneZmienne.Add(pair.Key, pair.Value);
                    }
                }
            }
            return false;
        }
    }
}
